3.6.2.2 Railway Control System

3.6.2.2 Railway Control System

In this example, we model a railway control system to automatically control trains passing a critical point such as a bridge. The idea is to use a computer to guide trains from several tracks crossing a single bridge instead of building many bridges. Obviously, a safety-property of such a system is to avoid the situation where more than one train are crossing the bridge at the same time.

For more details about this example, see [WangPD94].

The global declaration part
////////////////The Model//////////////////

#import "PAT.Lib.Queue";

//number of trains

#define N 4;

channel appr[N];

channel go[N];

channel leave[N];

channel stop[N];

var<Queue> queue;

clock x[N];

clock y;

In this example, we import the external C# library to use the queue functions. Constant N represents the nunber of trains. We define arrays of channels to represent the status of the N trains. Clock x[N] is an array which record the clock value of each train during the execution.

The process definition part

Train Process with paramenter i:

Gate process:

The whole system is defined as follows:

System = ||| z:{0..N-1}@Train(z) ||| Gate;

The asserstion part
////////////////////////////////////////////////////////////////////////////////////
#assert System deadlockfree;

//Whenever a train approaches the bridge, it will eventually cross.
#assert System |= []("appr[1]" -> <> "leave[1]"); //Notice: channel should be specified as a string eclosed within a pair of " ".

//overflow: There can never be N elements in the queue (thus the array will not overflow).
#define overflow (queue.Count()> N);
#assert System reaches overflow;